A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type, cond:(V:Type  (State(ds)V(A + Top))), k:Knd.
(hasloc(k;source(l)))  (trigger-send(A;ds;k;cond;l;tg)  Realizer) 

latex

Definitions

trigger-send(A;ds;x;cond;l;tg), t  T, x:A. B(x), source(l), hasloc(k;i), b, Realizer, P  Q, Knd, Type, State(ds), Top, left + right, x:AB(x), x:A  B(x), Id, a:A fp B(a), IdLnk, P & Q, P  Q, IdDeq, Atom$n, if b then t else f fi , s = t, tag(k), x.A(x), x. t(x), f  g, x : v, type List, (x  l), {x:A| B(x)} , , A, Unit, DeclaredType(ds;x), [], b, , f(x)?z, False, case b of inl(x) => s(x) | inr(y) => t(y), S  T, x:A.B(x), Void, f(a), let x,y = A in B(x;y), <a, b>, do-apply(f;x), [car / cdr], can-apply(f;x), isrcvl(l;k), Rsends(ds;knd;T;l;dt;g)

Lemmas

Rsends wf, isrcvl wf, bool wf, can-apply wf, do-apply wf, fpf-cap-single-join, fpf-cap-single1, fpf-join-cap-sq, fpf-cap-single, fpf-single-dom-sq, eqof eq btrue, fpf-cap wf, id-deq wf, top wf, bnot wf, not wf, ifthenelse wf, decl-type wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-single wf3, fpf-join wf, fpf-single wf, tagof wf, assert-isrcvl, assert-hasloc, assert wf, hasloc wf, lsrc wf